package AES
is
  MAXKC: constant Integer := 8;
  MAXNR: constant Integer := 14;

  type byte is mod 2 ** 8;
  subtype word_index is Integer range 0 .. 3;
  type word is array (word_index) of byte;

  type byte_table is array (byte) of byte;
  type word_table is array (byte) of word;
  subtype rcon_index is Integer range 0 .. 9;
  type rcon_array is array (rcon_index) of word;

  Logtable : constant byte_table := byte_table'(
  0,   0,  25,   1,  50,   2,  26, 198,  75, 199,  27, 104,  51, 238, 223,   3,
100,   4, 224,  14,  52, 141, 129, 239,  76, 113,   8, 200, 248, 105,  28, 193,
125, 194,  29, 181, 249, 185,  39, 106,  77, 228, 166, 114, 154, 201,   9, 120,
101,  47, 138,   5,  33,  15, 225,  36,  18, 240, 130,  69,  53, 147, 218, 142,
150, 143, 219, 189,  54, 208, 206, 148,  19,  92, 210, 241,  64,  70, 131,  56,
102, 221, 253,  48, 191,   6, 139,  98, 179,  37, 226, 152,  34, 136, 145,  16,
126, 110,  72, 195, 163, 182,  30,  66,  58, 107,  40,  84, 250, 133,  61, 186,
 43, 121,  10,  21, 155, 159,  94, 202,  78, 212, 172, 229, 243, 115, 167,  87,
175,  88, 168,  80, 244, 234, 214, 116,  79, 174, 233, 213, 231, 230, 173, 232,
 44, 215, 117, 122, 235,  22,  11, 245,  89, 203,  95, 176, 156, 169,  81, 160,
127,  12, 246, 111,  23, 196,  73, 236, 216,  67,  31,  45, 164, 118, 123, 183,
204, 187,  62,  90, 251,  96, 177, 134,  59,  82, 161, 108, 170,  85,  41, 157,
151, 178, 135, 144,  97, 190, 220, 252, 188, 149, 207, 205,  55,  63,  91, 209,
 83,  57, 132,  60,  65, 162, 109,  71,  20,  42, 158,  93,  86, 242, 211, 171,
 68,  17, 146, 217,  35,  32,  46, 137, 180, 124, 184,  38, 119, 153, 227, 165,
103,  74, 237, 222, 197,  49, 254,  24,  13,  99, 140, 128, 192, 247, 112,   7
);

  Alogtable : constant byte_table := byte_table'(
  1,   3,   5,  15,  17,  51,  85, 255,  26,  46, 114, 150, 161, 248,  19,  53,
 95, 225,  56,  72, 216, 115, 149, 164, 247,   2,   6,  10,  30,  34, 102, 170,
229,  52,  92, 228,  55,  89, 235,  38, 106, 190, 217, 112, 144, 171, 230,  49,
 83, 245,   4,  12,  20,  60,  68, 204,  79, 209, 104, 184, 211, 110, 178, 205,
 76, 212, 103, 169, 224,  59,  77, 215,  98, 166, 241,   8,  24,  40, 120, 136,
131, 158, 185, 208, 107, 189, 220, 127, 129, 152, 179, 206,  73, 219, 118, 154,
181, 196,  87, 249,  16,  48,  80, 240,  11,  29,  39, 105, 187, 214,  97, 163,
254,  25,  43, 125, 135, 146, 173, 236,  47, 113, 147, 174, 233,  32,  96, 160,
251,  22,  58,  78, 210, 109, 183, 194,  93, 231,  50,  86, 250,  21,  63,  65,
195,  94, 226,  61,  71, 201,  64, 192,  91, 237,  44, 116, 156, 191, 218, 117,
159, 186, 213, 100, 172, 239,  42, 126, 130, 157, 188, 223, 122, 142, 137, 128,
155, 182, 193,  88, 232,  35, 101, 175, 234,  37, 111, 177, 200,  67, 197,  84,
252,  31,  33,  99, 165, 244,   7,   9,  27,  45, 119, 153, 176, 203,  70, 202,
 69, 207,  74, 222, 121, 139, 134, 145, 168, 227,  62,  66, 198,  81, 243,  14,
 18,  54,  90, 238,  41, 123, 141, 140, 143, 138, 133, 148, 167, 242,  13,  23,
 57,  75, 221, 124, 132, 151, 162, 253,  28,  36, 108, 180, 199,  82, 246,   1
);

  S : constant byte_table := byte_table'(
 99, 124, 119, 123, 242, 107, 111, 197,  48,   1, 103,  43, 254, 215, 171, 118,
202, 130, 201, 125, 250,  89,  71, 240, 173, 212, 162, 175, 156, 164, 114, 192,
183, 253, 147,  38,  54,  63, 247, 204,  52, 165, 229, 241, 113, 216,  49,  21,
  4, 199,  35, 195,  24, 150,   5, 154,   7,  18, 128, 226, 235,  39, 178, 117,
  9, 131,  44,  26,  27, 110,  90, 160,  82,  59, 214, 179,  41, 227,  47, 132,
 83, 209,   0, 237,  32, 252, 177,  91, 106, 203, 190,  57,  74,  76,  88, 207,
208, 239, 170, 251,  67,  77,  51, 133,  69, 249,   2, 127,  80,  60, 159, 168,
 81, 163,  64, 143, 146, 157,  56, 245, 188, 182, 218,  33,  16, 255, 243, 210,
205,  12,  19, 236,  95, 151,  68,  23, 196, 167, 126,  61, 100,  93,  25, 115,
 96, 129,  79, 220,  34,  42, 144, 136,  70, 238, 184,  20, 222,  94,  11, 219,
224,  50,  58,  10,  73,   6,  36,  92, 194, 211, 172,  98, 145, 149, 228, 121,
231, 200,  55, 109, 141, 213,  78, 169, 108,  86, 244, 234, 101, 122, 174,   8,
186, 120,  37,  46,  28, 166, 180, 198, 232, 221, 116,  31,  75, 189, 139, 138,
112,  62, 181, 102,  72,   3, 246,  14,  97,  53,  87, 185, 134, 193,  29, 158,
225, 248, 152,  17, 105, 217, 142, 148, 155,  30, 135, 233, 206,  85,  40, 223,
140, 161, 137,  13, 191, 230,  66, 104,  65, 153,  45,  15, 176,  84, 187,  22
);

  Si : constant byte_table := byte_table'(
 82,   9, 106, 213,  48,  54, 165,  56, 191,  64, 163, 158, 129, 243, 215, 251,
124, 227,  57, 130, 155,  47, 255, 135,  52, 142,  67,  68, 196, 222, 233, 203,
 84, 123, 148,  50, 166, 194,  35,  61, 238,  76, 149,  11,  66, 250, 195,  78,
  8,  46, 161, 102,  40, 217,  36, 178, 118,  91, 162,  73, 109, 139, 209,  37,
114, 248, 246, 100, 134, 104, 152,  22, 212, 164,  92, 204,  93, 101, 182, 146,
108, 112,  72,  80, 253, 237, 185, 218,  94,  21,  70,  87, 167, 141, 157, 132,
144, 216, 171,   0, 140, 188, 211,  10, 247, 228,  88,   5, 184, 179,  69,   6,
208,  44,  30, 143, 202,  63,  15,   2, 193, 175, 189,   3,   1,  19, 138, 107,
 58, 145,  17,  65,  79, 103, 220, 234, 151, 242, 207, 206, 240, 180, 230, 115,
150, 172, 116,  34, 231, 173,  53, 133, 226, 249,  55, 232,  28, 117, 223, 110,
 71, 241,  26, 113,  29,  41, 197, 137, 111, 183,  98,  14, 170,  24, 190,  27,
252,  86,  62,  75, 198, 210, 121,  32, 154, 219, 192, 254, 120, 205,  90, 244,
 31, 221, 168,  51, 136,   7, 199,  49, 177,  18,  16,  89,  39, 128, 236,  95,
 96,  81, 127, 169,  25, 181,  74,  13,  45, 229, 122, 159, 147, 201, 156, 239,
160, 224,  59,  77, 174,  42, 245, 176, 200, 235, 187,  60, 131,  83, 153,  97,
 23,  43,   4, 126, 186, 119, 214,  38, 225, 105,  20,  99,  85,  33,  12, 125
);

  rcon: constant rcon_array := rcon_array'(
    word'(16#01#,16#00#,16#00#,16#00#), word'(16#02#,16#00#,16#00#,16#00#),
    word'(16#04#,16#00#,16#00#,16#00#), word'(16#08#,16#00#,16#00#,16#00#),
    word'(16#10#,16#00#,16#00#,16#00#), word'(16#20#,16#00#,16#00#,16#00#),
    word'(16#40#,16#00#,16#00#,16#00#), word'(16#80#,16#00#,16#00#,16#00#),
    word'(16#1B#,16#00#,16#00#,16#00#), word'(16#36#,16#00#,16#00#,16#00#)
  );

  subtype byte_index is Integer range 0 .. 15;
  type block is array (byte_index) of byte;

  subtype key_index is Integer range 0 .. 4*MAXKC-1;
  type key is array(key_index) of byte;
  subtype roundkey_index is Integer range 0 .. 4*(MAXNR+1)-1;
  type key_schedule is array(roundkey_index) of word;

  subtype state_index is Integer range 0 .. 3;
  type state is array(state_index) of word;

  function mul(a, b: byte) return byte;
  --# return r => ((a = 0 or b = 0) and r = 0) or
  --#             ((a /= 0 and b /= 0) and
  --#               r = Alogtable(byte((Integer(Logtable(a)) + Integer(Logtable(b))) mod 255)));

  function word_xor(a, b: word) return word;
  --# return word'(a(0) xor b(0), a(1) xor b(1), a(2) xor b(2), a(3) xor b(3));

  function word_xor_xor(a, b, c: word) return word;
  --# return word'(a(0) xor b(0) xor c(0),
  --#              a(1) xor b(1) xor c(1),
  --#              a(2) xor b(2) xor c(2),
  --#              a(3) xor b(3) xor c(3));

  function SubWord(w: word) return word;
  --# return word'(S(w(0)), S(w(1)), S(w(2)), S(w(3)));

  function RotWord(w: word) return word;
  --# return word'(w(1), w(2), w(3), w(0));

  function Block2State(t: block) return state;
  --# return state'(word'(t( 0), t( 1), t( 2), t( 3)),
  --#               word'(t( 4), t( 5), t( 6), t( 7)),
  --#               word'(t( 8), t( 9), t(10), t(11)),
  --#               word'(t(12), t(13), t(14), t(15)));

  function State2Block(st: state) return block;
  --# return block'(st(0)(0), st(0)(1), st(0)(2), st(0)(3),
  --#               st(1)(0), st(1)(1), st(1)(2), st(1)(3),
  --#               st(2)(0), st(2)(1), st(2)(2), st(2)(3),
  --#               st(3)(0), st(3)(1), st(3)(2), st(3)(3));

  function SubBytes(st: state) return state;
  --# return state'(word'(S(st(0)(0)), S(st(0)(1)), S(st(0)(2)), S(st(0)(3))),
  --#               word'(S(st(1)(0)), S(st(1)(1)), S(st(1)(2)), S(st(1)(3))),
  --#               word'(S(st(2)(0)), S(st(2)(1)), S(st(2)(2)), S(st(2)(3))),
  --#               word'(S(st(3)(0)), S(st(3)(1)), S(st(3)(2)), S(st(3)(3))));

  function InvSubBytes(st: state) return state;
  --# return state'(word'(Si(st(0)(0)), Si(st(0)(1)), Si(st(0)(2)), Si(st(0)(3))),
  --#               word'(Si(st(1)(0)), Si(st(1)(1)), Si(st(1)(2)), Si(st(1)(3))),
  --#               word'(Si(st(2)(0)), Si(st(2)(1)), Si(st(2)(2)), Si(st(2)(3))),
  --#               word'(Si(st(3)(0)), Si(st(3)(1)), Si(st(3)(2)), Si(st(3)(3))));

  function ShiftRows(st: state) return state;
  --# return state'(word'(st(0)(0), st(1)(1), st(2)(2), st(3)(3)),
  --#               word'(st(1)(0), st(2)(1), st(3)(2), st(0)(3)),
  --#               word'(st(2)(0), st(3)(1), st(0)(2), st(1)(3)),
  --#               word'(st(3)(0), st(0)(1), st(1)(2), st(2)(3)));

  function InvShiftRows(st: state) return state;
  --# return state'(word'(st(0)(0), st(3)(1), st(2)(2), st(1)(3)),
  --#               word'(st(1)(0), st(0)(1), st(3)(2), st(2)(3)),
  --#               word'(st(2)(0), st(1)(1), st(0)(2), st(3)(3)),
  --#               word'(st(3)(0), st(2)(1), st(1)(2), st(0)(3)));

  function MixColumns(st: state) return state;
  --# return state'(
  --#          word'(
  --#            mul(2, st(0)(0)) xor mul(3, st(0)(1)) xor        st(0)(2)  xor        st(0)(3) ,
  --#                   st(0)(0)  xor mul(2, st(0)(1)) xor mul(3, st(0)(2)) xor        st(0)(3) ,
  --#                   st(0)(0)  xor        st(0)(1)  xor mul(2, st(0)(2)) xor mul(3, st(0)(3)),
  --#            mul(3, st(0)(0)) xor        st(0)(1)  xor        st(0)(2)  xor mul(2, st(0)(3))),
  --#          word'(
  --#            mul(2, st(1)(0)) xor mul(3, st(1)(1)) xor        st(1)(2)  xor        st(1)(3) ,
  --#                   st(1)(0)  xor mul(2, st(1)(1)) xor mul(3, st(1)(2)) xor        st(1)(3) ,
  --#                   st(1)(0)  xor        st(1)(1)  xor mul(2, st(1)(2)) xor mul(3, st(1)(3)),
  --#            mul(3, st(1)(0)) xor        st(1)(1)  xor        st(1)(2)  xor mul(2, st(1)(3))),
  --#          word'(
  --#            mul(2, st(2)(0)) xor mul(3, st(2)(1)) xor        st(2)(2)  xor        st(2)(3) ,
  --#                   st(2)(0)  xor mul(2, st(2)(1)) xor mul(3, st(2)(2)) xor        st(2)(3) ,
  --#                   st(2)(0)  xor        st(2)(1)  xor mul(2, st(2)(2)) xor mul(3, st(2)(3)),
  --#            mul(3, st(2)(0)) xor        st(2)(1)  xor        st(2)(2)  xor mul(2, st(2)(3))),
  --#          word'(
  --#            mul(2, st(3)(0)) xor mul(3, st(3)(1)) xor        st(3)(2)  xor        st(3)(3) ,
  --#                   st(3)(0)  xor mul(2, st(3)(1)) xor mul(3, st(3)(2)) xor        st(3)(3) ,
  --#                   st(3)(0)  xor        st(3)(1)  xor mul(2, st(3)(2)) xor mul(3, st(3)(3)),
  --#            mul(3, st(3)(0)) xor        st(3)(1)  xor        st(3)(2)  xor mul(2, st(3)(3))));

  function InvMixColumns(st: state) return state;
  --# return state'(
  --#          word'(
  --#            mul(16#0e#, st(0)(0)) xor mul(16#0b#, st(0)(1)) xor mul(16#0d#, st(0)(2)) xor mul(16#09#, st(0)(3)),
  --#            mul(16#09#, st(0)(0)) xor mul(16#0e#, st(0)(1)) xor mul(16#0b#, st(0)(2)) xor mul(16#0d#, st(0)(3)),
  --#            mul(16#0d#, st(0)(0)) xor mul(16#09#, st(0)(1)) xor mul(16#0e#, st(0)(2)) xor mul(16#0b#, st(0)(3)),
  --#            mul(16#0b#, st(0)(0)) xor mul(16#0d#, st(0)(1)) xor mul(16#09#, st(0)(2)) xor mul(16#0e#, st(0)(3))),
  --#          word'(
  --#            mul(16#0e#, st(1)(0)) xor mul(16#0b#, st(1)(1)) xor mul(16#0d#, st(1)(2)) xor mul(16#09#, st(1)(3)),
  --#            mul(16#09#, st(1)(0)) xor mul(16#0e#, st(1)(1)) xor mul(16#0b#, st(1)(2)) xor mul(16#0d#, st(1)(3)),
  --#            mul(16#0d#, st(1)(0)) xor mul(16#09#, st(1)(1)) xor mul(16#0e#, st(1)(2)) xor mul(16#0b#, st(1)(3)),
  --#            mul(16#0b#, st(1)(0)) xor mul(16#0d#, st(1)(1)) xor mul(16#09#, st(1)(2)) xor mul(16#0e#, st(1)(3))),
  --#          word'(
  --#            mul(16#0e#, st(2)(0)) xor mul(16#0b#, st(2)(1)) xor mul(16#0d#, st(2)(2)) xor mul(16#09#, st(2)(3)),
  --#            mul(16#09#, st(2)(0)) xor mul(16#0e#, st(2)(1)) xor mul(16#0b#, st(2)(2)) xor mul(16#0d#, st(2)(3)),
  --#            mul(16#0d#, st(2)(0)) xor mul(16#09#, st(2)(1)) xor mul(16#0e#, st(2)(2)) xor mul(16#0b#, st(2)(3)),
  --#            mul(16#0b#, st(2)(0)) xor mul(16#0d#, st(2)(1)) xor mul(16#09#, st(2)(2)) xor mul(16#0e#, st(2)(3))),
  --#          word'(
  --#            mul(16#0e#, st(3)(0)) xor mul(16#0b#, st(3)(1)) xor mul(16#0d#, st(3)(2)) xor mul(16#09#, st(3)(3)),
  --#            mul(16#09#, st(3)(0)) xor mul(16#0e#, st(3)(1)) xor mul(16#0b#, st(3)(2)) xor mul(16#0d#, st(3)(3)),
  --#            mul(16#0d#, st(3)(0)) xor mul(16#09#, st(3)(1)) xor mul(16#0e#, st(3)(2)) xor mul(16#0b#, st(3)(3)),
  --#            mul(16#0b#, st(3)(0)) xor mul(16#0d#, st(3)(1)) xor mul(16#09#, st(3)(2)) xor mul(16#0e#, st(3)(3))));

  function AddRoundKey(st: state; rk0, rk1, rk2, rk3: in word) return state;
  --# return state'(
  --#          word'(st(0)(0) xor rk0(0), st(0)(1) xor rk0(1), st(0)(2) xor rk0(2), st(0)(3) xor rk0(3)),
  --#          word'(st(1)(0) xor rk1(0), st(1)(1) xor rk1(1), st(1)(2) xor rk1(2), st(1)(3) xor rk1(3)),
  --#          word'(st(2)(0) xor rk2(0), st(2)(1) xor rk2(1), st(2)(2) xor rk2(2), st(2)(3) xor rk2(3)),
  --#          word'(st(3)(0) xor rk3(0), st(3)(1) xor rk3(1), st(3)(2) xor rk3(2), st(3)(3) xor rk3(3)));

  function KeySetupEnc4(cipherKey: key) return key_schedule;
  --# return rk => (for all i in Integer range 0 .. 3 =>
  --#                (rk(i) = word'(cipherKey(4*i), cipherKey(4*i+1), cipherKey(4*i+2), cipherKey(4*i+3)))) and
  --#              (for all i in Integer range 4 .. 43 =>
  --#                ((i mod 4 = 0 and rk(i) = word_xor_xor(rk(i-4), SubWord(RotWord(rk(i-1))), rcon(i/4-1))) or
  --#                (i mod 4 /= 0 and rk(i) = word_xor(rk(i-4), rk(i-1)))));

  function KeySetupEnc6(cipherKey: key) return key_schedule;
  --# return rk => (for all i in Integer range 0 .. 5 =>
  --#                (rk(i) = word'(cipherKey(4*i), cipherKey(4*i+1), cipherKey(4*i+2), cipherKey(4*i+3)))) and
  --#              (for all i in Integer range 6 .. 51 =>
  --#                ((i mod 6 = 0 and rk(i) = word_xor_xor(rk(i-6), SubWord(RotWord(rk(i-1))), rcon(i/6-1))) or
  --#                (i mod 6 /= 0 and rk(i) = word_xor(rk(i-6), rk(i-1)))));

  function KeySetupEnc8(cipherKey: key) return key_schedule;
  --# return rk => (for all i in Integer range 0 .. 7 =>
  --#                (rk(i) = word'(cipherKey(4*i), cipherKey(4*i+1), cipherKey(4*i+2), cipherKey(4*i+3)))) and
  --#              (for all i in Integer range 8 .. 59 =>
  --#                ((i mod 8 = 0 and                  rk(i) = word_xor_xor(rk(i-8), SubWord(RotWord(rk(i-1))), rcon(i/8-1))) or
  --#                (i mod 8 /= 0 and i mod 4 = 0 and  rk(i) = word_xor(rk(i-8), SubWord(rk(i-1)))) or
  --#                (i mod 8 /= 0 and i mod 4 /= 0 and rk(i) = word_xor(rk(i-8), rk(i-1)))));

  function KeySetupEnc(cipherKey: key; Nk: Integer) return key_schedule;
  --# pre Nk = 4 or Nk = 6 or Nk = 8;
  --# return rk => (Nk = 4 and rk = KeySetupEnc4(cipherKey)) or
  --#              (Nk = 6 and rk = KeySetupEnc6(cipherKey)) or
  --#              (Nk = 8 and rk = KeySetupEnc8(cipherKey));

  function KeyScheduleMod1(W: key_schedule; Nr: Integer) return key_schedule;
  --# pre Nr = 10 or Nr = 12 or Nr = 14;
  --# return rk => (for all i in Integer range 0 .. Nr =>
  --#                (rk(4*i  ) = W(4*(Nr-i)  ) and
  --#                 rk(4*i+1) = W(4*(Nr-i)+1) and
  --#                 rk(4*i+2) = W(4*(Nr-i)+2) and
  --#                 rk(4*i+3) = W(4*(Nr-i)+3))) and
  --#              (for all j in Integer range 4*(Nr+1) .. 4*(MAXNR+1)-1 =>
  --#                (rk(j) = W(j)));

  function KeyScheduleMod2(W: key_schedule; Nr: Integer) return key_schedule;
  --# pre Nr = 10 or Nr = 12 or Nr = 14;
  --# return rk => (for all i in Integer range 1 .. Nr-1 =>
  --#                (rk(4*i  ) = InvMixColumns(state'(W(4*i), W(4*i+1), W(4*i+2), W(4*i+3)))(0) and
  --#                 rk(4*i+1) = InvMixColumns(state'(W(4*i), W(4*i+1), W(4*i+2), W(4*i+3)))(1) and
  --#                 rk(4*i+2) = InvMixColumns(state'(W(4*i), W(4*i+1), W(4*i+2), W(4*i+3)))(2) and
  --#                 rk(4*i+3) = InvMixColumns(state'(W(4*i), W(4*i+1), W(4*i+2), W(4*i+3)))(3))) and
  --#              (for all j in Integer range 0 .. 3 =>
  --#                (rk(j) = W(j))) and
  --#              (for all j in Integer range 4*Nr .. 4*(MAXNR+1)-1 =>
  --#                (rk(j) = W(j)));

  function KeySetupDec(cipherKey: key; Nk: in Integer) return key_schedule;
  --# pre Nk = 4 or Nk = 6 or Nk = 8;
  --# return KeyScheduleMod2(KeyScheduleMod1(KeySetupEnc(cipherKey, Nk), Nk+6), Nk+6);

  procedure aesKeySetupEnc(rk: out key_schedule; cipherKey: in key; keyBits: in Integer; Nr: out Integer);
  --# derives rk from cipherKey, keyBits &
  --#         Nr from keyBits;
  --# pre keyBits = 128 or keyBits = 192 or keyBits = 256;
  
  --# tvn: invariants 
  --# post Nr = keyBits/32 + 6 and
  --#      rk = KeySetupEnc(cipherKey, keyBits/32);

  procedure aesKeySetupDec(rk: out key_schedule; cipherKey: in key; keyBits: in Integer; Nr: out Integer);
  --# derives rk from cipherKey, keyBits &
  --#         Nr from keyBits;
  --# pre keyBits = 128 or keyBits = 192 or keyBits = 256;
  
  --# tvn: invariants
  --# post Nr = keyBits/32 + 6 and
  --#      rk = KeySetupDec(cipherKey, keyBits/32);

  --# function encrypt_round(st: state; rk: key_schedule; Nr: Integer; r: Integer) return state;

  --# function decrypt_round(st: state; rk: key_schedule; Nr: Integer; r: Integer) return state;

  procedure aesEncrypt(rk: in key_schedule; Nr: in Integer; pt: in block; ct: out block);
  --# derives ct from pt, rk, Nr;
  --# pre Nr = 10 or Nr = 12 or Nr = 14;
  --# post ct = State2Block(encrypt_round(Block2State(pt), rk, Nr, Nr));

  procedure aesDecrypt(rk: in key_schedule; Nr: in Integer; ct: in block; pt: out block);
  --# derives pt from ct, rk, Nr;
  --# pre Nr = 10 or Nr = 12 or Nr = 14;
  --# post pt = State2Block(decrypt_round(Block2State(ct), rk, Nr, Nr));

end AES;

-- Properties of encrypt_round() defined in rule file:
-- (1) r = 0 => encrypt_round(st, rk, Nr, 0) may_be_replaced_by
--                AddRoundKey(st, rk(0), rk(1), rk(2), rk(3))
-- (2) r > 0 and r < Nr => encrypt_round(st, rk, Nr, r) may_be_replaced_by
--                           AddRoundKey(
--                             MixColumns(
--                               ShiftRows(
--                                 SubBytes(
--                                   encrypt_round(st, rk, Nr, r-1)
--                                 )
--                               )
--                             ), rk(4*r), rk(4*r+1), rk(4*r+2), rk(4*r+3)
--                           )
-- (3) r = Nr => encrypt_round(st, rk, Nr, Nr) may_be_replaced_by
--                 AddRoundKey(
--                   ShiftRows(
--                     SubBytes(
--                       encrypt_round(st, rk, Nr, Nr-1)
--                     )
--                   ), rk(4*Nr), rk(4*Nr+1), rk(4*Nr+2), rk(4*Nr+3)
--                 )

-- Properties of decrypt_round() defined in rule file:
-- (1) r = 0 => decrypt_round(st, rk, Nr, 0) may_be_replaced_by
--                AddRoundKey(st, rk(0), rk(1), rk(2), rk(3))
-- (2) r > 0 and r < Nr => decrypt_round(st, rk, Nr, r) may_be_replaced_by
--                           AddRoundKey(
--                             InvMixColumns(
--                               InvShiftRows(
--                                 InvSubBytes(
--                                   decrypt_round(st, rk, Nr, r-1)
--                                 )
--                               )
--                             ), rk(4*r), rk(4*r+1), rk(4*r+2), rk(4*r+3)
--                           )
-- (3) r = Nr => decrypt_round(st, rk, Nr, Nr) may_be_replaced_by
--                 AddRoundKey(
--                   InvShiftRows(
--                     InvSubBytes(
--                       decrypt_round(st, rk, Nr, Nr-1)
--                     )
--                   ), rk(4*Nr), rk(4*Nr+1), rk(4*Nr+2), rk(4*Nr+3)
--                 )
